InforLorV4, Main, Exploration, bibRecord, 00B338

Observational proofs with critical contexts

Identifieur interne : 00B338 ( Main/Exploration ); précédent : 00B337; suivant : 00B339

Observational proofs with critical contexts

Auteurs : Narjes Berregeb [France] ; Adel Bouhoula [France] ; Michaël Rusinowitch [France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:29F83BB865C031B83CAD4F353A2B4F53DB3BB4A3

Descripteurs français

Pascal (Inist)
- Informatique théorique, Spécification algébrique, Système réécriture, Théorie programmation.

English descriptors

KwdEn :
- Algebraic specification, Computer theory, Programming theory, Rewriting systems.

Abstract

Abstract: Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.

Url:

https://api.istex.fr/ark:/67375/HCB-LRF9D0DZ-2/fulltext.pdf

DOI: 10.1007/BFb0053582

Affiliations:

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Observational proofs with critical contexts</title>
<author><name sortKey="Berregeb, Narjes" sort="Berregeb, Narjes" uniqKey="Berregeb N" first="Narjes" last="Berregeb">Narjes Berregeb</name>
</author>
<author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:29F83BB865C031B83CAD4F353A2B4F53DB3BB4A3</idno>
<date when="1998" year="1998">1998</date>
<idno type="doi">10.1007/BFb0053582</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-LRF9D0DZ-2/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000975</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000975</idno>
<idno type="wicri:Area/Istex/Curation">000969</idno>
<idno type="wicri:Area/Istex/Checkpoint">002570</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002570</idno>
<idno type="wicri:doubleKey">0302-9743:1998:Berregeb N:observational:proofs:with</idno>
<idno type="wicri:Area/Main/Merge">00BA60</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:98-0233935</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000C04</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000C70</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000B41</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000B41</idno>
<idno type="wicri:doubleKey">0302-9743:1998:Berregeb N:observational:proofs:with</idno>
<idno type="wicri:Area/Main/Merge">00BB63</idno>
<idno type="wicri:Area/Main/Curation">00B338</idno>
<idno type="wicri:Area/Main/Exploration">00B338</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Observational proofs with critical contexts</title>
<author><name sortKey="Berregeb, Narjes" sort="Berregeb, Narjes" uniqKey="Berregeb N" first="Narjes" last="Berregeb">Narjes Berregeb</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Villers-lès-Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Villers-lès-Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA - INRIA Lorraine, 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Villers-lès-Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<title level="s" type="abbrev">Lect Notes Comput Sci</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algebraic specification</term>
<term>Computer theory</term>
<term>Programming theory</term>
<term>Rewriting systems</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Informatique théorique</term>
<term>Spécification algébrique</term>
<term>Système réécriture</term>
<term>Théorie programmation</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker [10]. We propose in this paper to embed Context Induction in the implicit induction framework of [8]. The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Villers-lès-Nancy</li>
</settlement>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Berregeb, Narjes" sort="Berregeb, Narjes" uniqKey="Berregeb N" first="Narjes" last="Berregeb">Narjes Berregeb</name>
</region>
<name sortKey="Berregeb, Narjes" sort="Berregeb, Narjes" uniqKey="Berregeb N" first="Narjes" last="Berregeb">Narjes Berregeb</name>
<name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name>
<name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name>
<name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
<name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00B338 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00B338 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:29F83BB865C031B83CAD4F353A2B4F53DB3BB4A3
   |texte=   Observational proofs with critical contexts
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

Serveur d'exploration sur la recherche en informatique en Lorraine

Observational proofs with critical contexts

Observational proofs with critical contexts

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.